
open Cub

let s = {
  type_defs = [ ("t_abst_1", []); ("t_const_1", ["Const1"; "Const2"]) ];
  decls = [ Dglobal ("var1", "proc");
            Dconst ("const1", "int");
            Darray ("array1", ("proc", "int")) ];
  init = (Some "z", SAtom.singleton
    (Atom.Comp (Access ("x", "p", Glob), Eq, Elem ("y", Glob))));
  invs = [ (["x"; "y"], SAtom.empty) ];
  unsafe = [ (["x"; "y"], SAtom.empty) ];
  trans = [ {
    tr_name = "trans1";
    tr_args = [ "x"; "y" ];
    tr_reqs = SAtom.singleton Atom.True;
    tr_ureq = [ ("", [ SAtom.empty ]) ];
    tr_actions = [
      Anondet "p";
      Aassign ("v", Const (ConstInt (Num.num_of_string "1")));
      Aupd { up_arr = "array1"; up_arg = "idx";
        up_swts = [
          (SAtom.singleton Atom.True,
           Arith ("z", Glob, ConstInt (Num.num_of_string "2")))
        ] } ]
  } ]
}

let _ =
  print_system Format.std_formatter s
